Termination proof of /tmp/tmp2XrkSU/Test7.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇒)

↳2 JBCTerminationGraph

↳3 FIGtoITRSProof (⇒)

↳4 AND

    ↳5 IDP

        ↳6 IDPNonInfProof (⇒)

        ↳7 AND

            ↳8 IDP

                ↳9 IDependencyGraphProof (⇔)

                ↳10 TRUE

            ↳11 IDP

                ↳12 IDependencyGraphProof (⇔)

                ↳13 TRUE

    ↳14 IDP

        ↳15 IDPtoQDPProof (⇒)

        ↳16 QDP

        ↳17 UsableRulesProof (⇔)

        ↳18 QDP

        ↳19 QReductionProof (⇔)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔)

        ↳22 YES

    ↳23 IDP

        ↳24 IDPNonInfProof (⇒)

        ↳25 AND

            ↳26 IDP

                ↳27 IDependencyGraphProof (⇔)

                ↳28 TRUE

            ↳29 IDP

                ↳30 IDependencyGraphProof (⇔)

                ↳31 TRUE

    ↳32 IDP

        ↳33 IDPNonInfProof (⇒)

        ↳34 AND

            ↳35 IDP

                ↳36 IDependencyGraphProof (⇔)

                ↳37 IDP

                ↳38 UsableRulesProof (⇔)

                ↳39 IDP

                ↳40 IDPNonInfProof (⇒)

                ↳41 AND

                    ↳42 IDP

                        ↳43 IDependencyGraphProof (⇔)

                        ↳44 TRUE

                    ↳45 IDP

                        ↳46 IDependencyGraphProof (⇔)

                        ↳47 TRUE

            ↳48 IDP

                ↳49 IDependencyGraphProof (⇔)

                ↳50 IDP

                ↳51 UsableRulesProof (⇔)

                ↳52 IDP

                ↳53 IDPNonInfProof (⇒)

                ↳54 AND

                    ↳55 IDP

                        ↳56 IDependencyGraphProof (⇔)

                        ↳57 TRUE

                    ↳58 IDP

                        ↳59 IDependencyGraphProof (⇔)

                        ↳60 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: Test7

public class Test7 {
    public static void main(String[] args) {
	List[] ls = { List.mk(args.length), List.mk(args.length), List.mk(args.length) };

	for (int k = 0; k < ls.length; k++) {
	    int len = length(ls[0]);
	    for (int i = 0; i < len; i++)
		bubble(ls[0]);
	}
    }

    private static void bubble(List l) {
	for (List cursor = l; cursor != null && cursor.getTail() != null; cursor = cursor.getTail())
	    if (cursor.head > cursor.getTail().head) {
		int temp = cursor.head;
		cursor.head = cursor.getTail().head;
		cursor.getTail().head = temp;
	    }
    }

    private static int length(List list) {
	int len = 0;

	while (list != null) {
	    list = list.getTail();
	    len++;
	}

	return len;
    }
}

public class List {
    public int head;
    private List tail;

    public List(int head, List tail) {
	this.head = head;
	this.tail = tail;
    }

    public List getTail() {
	return tail;
    }

    public static List mk(int len) {
	List result = null;

	while (len-- > 0)
	    result = new List(len, result);

	return result;
    }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Test7.main([Ljava/lang/String;)V: Graph of 81 nodes with 1 SCC.

List.mk(I)LList;: Graph of 30 nodes with 1 SCC.

Test7.length(LList;)I: Graph of 27 nodes with 1 SCC.

Test7.bubble(LList;)V: Graph of 137 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

Log for SCC 0:

Generated 131 rules for P and 8 rules for R.

Combined rules. Obtained 6 rules for P and 1 rules for R.

Filtered ground terms:

5157_0_bubble_Load(x1, x2) → 5157_0_bubble_Load(x2)
List(x1, x2, x3) → List(x2, x3)
Cond_3413_0_bubble_NULL3(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL3(x1, x3, x4)
3413_0_bubble_NULL(x1, x2, x3) → 3413_0_bubble_NULL(x2, x3)
5185_0_bubble_Load(x1, x2) → 5185_0_bubble_Load(x2)
Cond_3413_0_bubble_NULL2(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL2(x1, x3, x4)
Cond_3413_0_bubble_NULL1(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL1(x1, x3, x4)
Cond_3413_0_bubble_NULL(x1, x2, x3, x4) → Cond_3413_0_bubble_NULL(x1, x3, x4)
3425_0_bubble_Return(x1) → 3425_0_bubble_Return

Filtered duplicate args:

Cond_3413_0_bubble_NULL3(x1, x2, x3) → Cond_3413_0_bubble_NULL3(x1, x3)
3413_0_bubble_NULL(x1, x2) → 3413_0_bubble_NULL(x2)
Cond_3413_0_bubble_NULL2(x1, x2, x3) → Cond_3413_0_bubble_NULL2(x1, x3)
Cond_3413_0_bubble_NULL1(x1, x2, x3) → Cond_3413_0_bubble_NULL1(x1, x3)
Cond_3413_0_bubble_NULL(x1, x2, x3) → Cond_3413_0_bubble_NULL(x1, x3)

Combined rules. Obtained 6 rules for P and 1 rules for R.

Finished conversion. Obtained 6 rules for P and 1 rules for R. System has predefined symbols.

Log for SCC 1:

Generated 19 rules for P and 3 rules for R.

Combined rules. Obtained 3 rules for P and 1 rules for R.

Filtered ground terms:

816_0_length_Store(x1, x2) → 816_0_length_Store(x2)
732_0_length_NULL(x1, x2, x3) → 732_0_length_NULL(x2, x3)
List(x1, x2) → List(x2)
775_0_length_Return(x1) → 775_0_length_Return

Filtered duplicate args:

732_0_length_NULL(x1, x2) → 732_0_length_NULL(x2)

Finished conversion. Obtained 3 rules for P and 1 rules for R. System has no predefined symbols.

Log for SCC 2:

Generated 21 rules for P and 3 rules for R.

Combined rules. Obtained 1 rules for P and 0 rules for R.

Filtered ground terms:

398_0_mk_Inc(x1, x2, x3, x4) → 398_0_mk_Inc(x2, x3, x4)
List(x1) → List
java.lang.Object(x1) → java.lang.Object
Cond_398_0_mk_Inc(x1, x2, x3, x4, x5) → Cond_398_0_mk_Inc(x1, x3, x4, x5)

Filtered duplicate args:

398_0_mk_Inc(x1, x2, x3) → 398_0_mk_Inc(x2, x3)
Cond_398_0_mk_Inc(x1, x2, x3, x4) → Cond_398_0_mk_Inc(x1, x3, x4)

Filtered unneeded arguments:

398_0_mk_Inc(x1, x2) → 398_0_mk_Inc(x2)
Cond_398_0_mk_Inc(x1, x2, x3) → Cond_398_0_mk_Inc(x1, x3)

Combined rules. Obtained 1 rules for P and 0 rules for R.

Finished conversion. Obtained 1 rules for P and 0 rules for R. System has predefined symbols.

Log for SCC 3:

Generated 36 rules for P and 176 rules for R.

Combined rules. Obtained 4 rules for P and 22 rules for R.

Filtered ground terms:

1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → 1190_0_main_GE(x2, x3, x4, x5, x6, x7)
ARRAY(x1, x2) → ARRAY(x2)
Cond_1243_1_main_InvokeMethod(x1, x2, x3, x4, x5, x6, x7) → Cond_1243_1_main_InvokeMethod(x1, x3, x4, x5, x6, x7)
3425_0_bubble_Return(x1) → 3425_0_bubble_Return
1243_0_bubble_Load(x1, x2) → 1243_0_bubble_Load(x2)
Cond_1190_0_main_GE1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_1190_0_main_GE1(x1, x3, x4, x5, x6, x7, x8)
893_0_length_ConstantStackPush(x1, x2) → 893_0_length_ConstantStackPush(x2)
Cond_1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_1190_0_main_GE(x1, x3, x4, x5, x6, x7, x8)
775_0_length_Return(x1, x2) → 775_0_length_Return(x2)
3513_0_bubble_Return(x1) → 3513_0_bubble_Return
732_0_length_NULL(x1, x2, x3, x4) → 732_0_length_NULL(x2, x3, x4)
Cond_732_0_length_NULL(x1, x2, x3, x4, x5) → Cond_732_0_length_NULL(x1, x4)
List(x1) → List
Cond_805_1_length_InvokeMethod(x1, x2, x3, x4) → Cond_805_1_length_InvokeMethod(x1, x2, x3)
805_0_getTail_Return(x1, x2) → 805_0_getTail_Return(x2)
805_1_length_InvokeMethod(x1, x2, x3) → 805_1_length_InvokeMethod(x1, x2)
3413_0_bubble_NULL(x1, x2, x3) → 3413_0_bubble_NULL(x2, x3)
Cond_3746_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3746_0_bubble_LE(x1, x4, x5)
3746_0_bubble_LE(x1, x2, x3, x4) → 3746_0_bubble_LE(x3, x4)
Cond_3738_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3738_0_bubble_LE(x1, x4, x5)
3738_0_bubble_LE(x1, x2, x3, x4) → 3738_0_bubble_LE(x3, x4)
Cond_3756_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3756_0_bubble_LE(x1, x4, x5)
3756_0_bubble_LE(x1, x2, x3, x4) → 3756_0_bubble_LE(x3, x4)
Cond_3752_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3752_0_bubble_LE(x1, x4, x5)
3752_0_bubble_LE(x1, x2, x3, x4) → 3752_0_bubble_LE(x3, x4)
Cond_3728_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3728_0_bubble_LE(x1, x4, x5)
3728_0_bubble_LE(x1, x2, x3, x4) → 3728_0_bubble_LE(x3, x4)
Cond_3723_0_bubble_LE(x1, x2, x3, x4, x5) → Cond_3723_0_bubble_LE(x1, x4, x5)
3723_0_bubble_LE(x1, x2, x3, x4) → 3723_0_bubble_LE(x3, x4)

Filtered duplicate args:

1190_0_main_GE(x1, x2, x3, x4, x5, x6) → 1190_0_main_GE(x1, x2, x5, x6)
Cond_1190_0_main_GE1(x1, x2, x3, x4, x5, x6, x7) → Cond_1190_0_main_GE1(x1, x2, x3, x6, x7)
Cond_1190_0_main_GE(x1, x2, x3, x4, x5, x6, x7) → Cond_1190_0_main_GE(x1, x2, x3, x6, x7)
732_0_length_NULL(x1, x2, x3) → 732_0_length_NULL(x2, x3)
3413_0_bubble_NULL(x1, x2) → 3413_0_bubble_NULL(x2)

Filtered unneeded arguments:

Cond_1190_0_main_GE(x1, x2, x3, x4, x5) → Cond_1190_0_main_GE(x1, x2, x3)
Cond_3723_0_bubble_LE(x1, x2, x3) → Cond_3723_0_bubble_LE(x1)
Cond_3728_0_bubble_LE(x1, x2, x3) → Cond_3728_0_bubble_LE(x1)
Cond_3752_0_bubble_LE(x1, x2, x3) → Cond_3752_0_bubble_LE(x1)
Cond_3756_0_bubble_LE(x1, x2, x3) → Cond_3756_0_bubble_LE(x1)
Cond_3738_0_bubble_LE(x1, x2, x3) → Cond_3738_0_bubble_LE(x1)
Cond_3746_0_bubble_LE(x1, x2, x3) → Cond_3746_0_bubble_LE(x1)

Combined rules. Obtained 4 rules for P and 22 rules for R.

Finished conversion. Obtained 4 rules for P and 22 rules for R. System has predefined symbols.

(4) Complex Obligation (AND)

(5) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(x2[0] <= x1[0], java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
(1): COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
(2): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(x2[2] > x1[2], java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
(3): COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
(4): 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))
(5): 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(x2[5] > x1[5], java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))
(6): COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

(0) -> (1), if ((x2[0] <= x1[0] →^* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) →^* java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))))

(1) -> (0), if ((java.lang.Object(List(x0[1], x1[1])) →^* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(1) -> (2), if ((java.lang.Object(List(x0[1], x1[1])) →^* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(1) -> (5), if ((java.lang.Object(List(x0[1], x1[1])) →^* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(2) -> (3), if ((x2[2] > x1[2] →^* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) →^* java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))))

(3) -> (0), if ((java.lang.Object(List(x0[3], x2[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(3) -> (2), if ((java.lang.Object(List(x0[3], x2[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(3) -> (5), if ((java.lang.Object(List(x0[3], x2[3])) →^* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(4) -> (0), if ((java.lang.Object(List(x0[4], x1[4])) →^* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))))

(4) -> (2), if ((java.lang.Object(List(x0[4], x1[4])) →^* java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))))

(4) -> (5), if ((java.lang.Object(List(x0[4], x1[4])) →^* java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))))

(5) -> (6), if ((x2[5] > x1[5] →^* TRUE)∧(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) →^* java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))))

(6) -> (4), if ((java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])) →^* java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(6) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))) which results in the following constraint:
(1)    (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))

We simplified constraint (1) using rules (I), (II), (IV) which results in the following new constraint:
(2)    (<=(x2[0], x1[0])=TRUE ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))≥COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧[(20)bni_23 + (-1)Bound*bni_23] + [(16)bni_23]x0[0] ≥ 0∧[1 + (-1)bso_24] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(20)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_24] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:
(7)    (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x2[0]1)) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (7) using rules (I), (II), (III), (IV) which results in the following new constraint:
(8)    (<=(x2[0], x1[0])=TRUE ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0]1, x1[0]1)), x1[0])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(9)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(10)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(11)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[0]1 ≥ 0∧[63 + (-1)bso_26] + [48]x0[0]1 ≥ 0)

We simplified constraint (11) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(12)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:
(13)    (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (13) using rules (I), (II), (III), (IV) which results in the following new constraint:
(14)    (<=(x2[0], x1[0])=TRUE ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x1[0])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[2] ≥ 0∧[63 + (-1)bso_26] + [48]x0[2] ≥ 0)

We simplified constraint (17) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(18)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))), COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:
(19)    (<=(x2[0], x1[0])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))=java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))∧java.lang.Object(List(x0[1], x1[1]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (19) using rules (I), (II), (III), (IV) which results in the following new constraint:
(20)    (<=(x2[0], x1[0])=TRUE ⇒ COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])), x2[0])))≥NonInfC∧COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])), x2[0])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[0])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧[(83)bni_25 + (-1)Bound*bni_25] + [(64)bni_25]x0[5] ≥ 0∧[63 + (-1)bso_26] + [48]x0[5] ≥ 0)

We simplified constraint (23) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(24)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)

For Pair 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL1(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))) which results in the following constraint:
(25)    (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))

We simplified constraint (25) using rules (I), (II), (IV) which results in the following new constraint:
(26)    (>(x2[2], x1[2])=TRUE ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))≥COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥))

We simplified constraint (26) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(27)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (27) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(28)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (28) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(29)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧[(20)bni_27 + (-1)Bound*bni_27] + [(16)bni_27]x0[2] ≥ 0∧[1 + (-1)bso_28] ≥ 0)

We simplified constraint (29) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(30)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_27] ≥ 0∧[(20)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_28] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x2))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:
(31)    (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (31) using rules (I), (II), (III), (IV) which results in the following new constraint:
(32)    (>(x2[2], x1[2])=TRUE ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[2])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (32) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(33)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

We simplified constraint (33) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(34)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

We simplified constraint (34) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(35)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[0] ≥ 0∧[63 + (-1)bso_30] + [48]x0[0] ≥ 0)

We simplified constraint (35) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(36)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:
(37)    (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2]1)) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (37) using rules (I), (II), (III), (IV) which results in the following new constraint:
(38)    (>(x2[2], x1[2])=TRUE ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2]1, x1[2]1)), x2[2])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (38) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(39)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

We simplified constraint (39) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(40)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

We simplified constraint (40) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(41)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[2]1 ≥ 0∧[63 + (-1)bso_30] + [48]x0[2]1 ≥ 0)

We simplified constraint (41) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(42)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))), COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:
(43)    (>(x2[2], x1[2])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))=java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))∧java.lang.Object(List(x0[3], x2[3]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (43) using rules (I), (II), (III), (IV) which results in the following new constraint:
(44)    (>(x2[2], x1[2])=TRUE ⇒ COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[2])), x2[2])))≥NonInfC∧COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x1[2])), x2[2])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[2])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥))

We simplified constraint (44) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(45)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

We simplified constraint (45) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(46)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

We simplified constraint (46) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(47)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧[(83)bni_29 + (-1)Bound*bni_29] + [(64)bni_29]x0[5] ≥ 0∧[63 + (-1)bso_30] + [48]x0[5] ≥ 0)

We simplified constraint (47) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(48)    (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)

For Pair 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1))) the following chains were created:

We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) which results in the following constraint:
(49)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (49) using rules (I), (II), (III), (IV) which results in the following new constraint:
(50)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[6])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (50) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(51)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

We simplified constraint (51) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(52)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

We simplified constraint (52) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(53)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[0] ≥ 0)

We simplified constraint (53) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(54)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) which results in the following constraint:
(55)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (55) using rules (I), (II), (III), (IV) which results in the following new constraint:
(56)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[6])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (56) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(57)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

We simplified constraint (57) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(58)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

We simplified constraint (58) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(59)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[2] ≥ 0)

We simplified constraint (59) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(60)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
We consider the chain COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))), 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) which results in the following constraint:
(61)    (java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))∧java.lang.Object(List(x0[4], x1[4]))=java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])) ⇒ 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (61) using rules (I), (II), (III), (IV) which results in the following new constraint:
(62)    (5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])), x1[6])))≥NonInfC∧5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])), x1[6])))≥3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[6])))∧(U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥))

We simplified constraint (62) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(63)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

We simplified constraint (63) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(64)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

We simplified constraint (64) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(65)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧[63 + (-1)bso_32] + [48]x0[5] ≥ 0)

We simplified constraint (65) using rules (IDP_UNRESTRICTED_VARS), (IDP_POLY_GCD) which results in the following new constraint:
(66)    ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)

For Pair 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL2(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))), COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))) which results in the following constraint:
(67)    (>(x2[5], x1[5])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))=java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])) ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥))

We simplified constraint (67) using rules (I), (II), (IV) which results in the following new constraint:
(68)    (>(x2[5], x1[5])=TRUE ⇒ 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))∧(U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥))

We simplified constraint (68) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(69)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

We simplified constraint (69) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(70)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

We simplified constraint (70) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(71)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧[(20)bni_33 + (-1)Bound*bni_33] + [(16)bni_33]x0[5] ≥ 0∧[1 + (-1)bso_34] ≥ 0)

We simplified constraint (71) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(72)    (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_33] ≥ 0∧[(20)bni_33 + (-1)Bound*bni_33] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_34] ≥ 0)

For Pair COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1))) the following chains were created:

We consider the chain 3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))), COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))), 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4]))) which results in the following constraint:
(73)    (>(x2[5], x1[5])=TRUE∧java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))=java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))∧java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6]))=java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4])) ⇒ COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥NonInfC∧COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6])))≥5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))∧(U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥))

We simplified constraint (73) using rules (I), (II), (III), (IV) which results in the following new constraint:
(74)    (>(x2[5], x1[5])=TRUE ⇒ COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥NonInfC∧COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))≥5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[5], x2[5])), x1[5])))∧(U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥))

We simplified constraint (74) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(75)    (0 ≥ 0 ⇒ (U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

We simplified constraint (75) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(76)    (0 ≥ 0 ⇒ (U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

We simplified constraint (76) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(77)    (0 ≥ 0 ⇒ (U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧[(19)bni_35 + (-1)Bound*bni_35] + [(16)bni_35]x0[5] ≥ 0∧[(-1)bso_36] ≥ 0)

We simplified constraint (77) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(78)    (0 ≥ 0 ⇒ (U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_35] ≥ 0∧[(19)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_36] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL(<=(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_23] ≥ 0∧[(20)bni_23 + (-1)Bound*bni_23] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_24] ≥ 0)
COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)))
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_25] ≥ 0∧[(83)bni_25 + (-1)Bound*bni_25] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_26] ≥ 0∧[1] ≥ 0)
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL1(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_27] ≥ 0∧[(20)bni_27 + (-1)Bound*bni_27] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_28] ≥ 0)
COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x2)))
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
- (0 ≥ 0 ⇒ (U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(64)bni_29] ≥ 0∧[(83)bni_29 + (-1)Bound*bni_29] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_30] ≥ 0∧[1] ≥ 0)
5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0, x1)))
- ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
- ((U^Increasing(3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))), ≥)∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[63 + (-1)bso_32] ≥ 0∧[1] ≥ 0)
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → COND_3413_0_BUBBLE_NULL2(>(x2, x1), java.lang.Object(List(java.lang.Object(List(x0, x1)), x2)))
- (0 ≥ 0 ⇒ (U^Increasing(COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_33] ≥ 0∧[(20)bni_33 + (-1)Bound*bni_33] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[1 + (-1)bso_34] ≥ 0)
COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0, x2)), x1)))
- (0 ≥ 0 ⇒ (U^Increasing(5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))), ≥)∧0 ≥ 0∧0 ≥ 0∧[(16)bni_35] ≥ 0∧[(19)bni_35 + (-1)Bound*bni_35] ≥ 0∧0 ≥ 0∧0 ≥ 0∧0 ≥ 0∧[(-1)bso_36] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers with natural coefficients for non-tuple symbols [NONINF][POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(3413_0_bubble_NULL(x₁)) = 0
POL(NULL) = 0
POL(3425_0_bubble_Return) = 0
POL(3413_0_BUBBLE_NULL(x₁)) = x₁
POL(java.lang.Object(x₁)) = [2]x₁
POL(List(x₁, x₂)) = [2] + [2]x₁
POL(COND_3413_0_BUBBLE_NULL(x₁, x₂)) = [-1] + x₂
POL(<=(x₁, x₂)) = 0
POL(COND_3413_0_BUBBLE_NULL1(x₁, x₂)) = [-1] + x₂
POL(>(x₁, x₂)) = 0
POL(5185_0_BUBBLE_LOAD(x₁)) = [-1] + x₁
POL(COND_3413_0_BUBBLE_NULL2(x₁, x₂)) = [-1] + x₂

The following pairs are in P_>:

3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))

The following pairs are in P_bound:

3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → COND_3413_0_BUBBLE_NULL(<=(x2[0], x1[0]), java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))
COND_3413_0_BUBBLE_NULL(TRUE, java.lang.Object(List(java.lang.Object(List(x0[1], x1[1])), x2[1]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[1], x1[1])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2]))) → COND_3413_0_BUBBLE_NULL1(>(x2[2], x1[2]), java.lang.Object(List(java.lang.Object(List(x0[2], x1[2])), x2[2])))
COND_3413_0_BUBBLE_NULL1(TRUE, java.lang.Object(List(java.lang.Object(List(x0[3], x1[3])), x2[3]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[3], x2[3])))
3413_0_BUBBLE_NULL(java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5]))) → COND_3413_0_BUBBLE_NULL2(>(x2[5], x1[5]), java.lang.Object(List(java.lang.Object(List(x0[5], x1[5])), x2[5])))
COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

The following pairs are in P_≥:

COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

There are no usable rules.

(7) Complex Obligation (AND)

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_3413_0_BUBBLE_NULL2(TRUE, java.lang.Object(List(java.lang.Object(List(x0[6], x1[6])), x2[6]))) → 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[6], x2[6])), x1[6])))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(9) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(10) TRUE

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(4): 5185_0_BUBBLE_LOAD(java.lang.Object(List(java.lang.Object(List(x0[4], x1[4])), x2[4]))) → 3413_0_BUBBLE_NULL(java.lang.Object(List(x0[4], x1[4])))

The set Q consists of the following terms:
3413_0_bubble_NULL(NULL)

(12) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(13) TRUE

(14) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:
none

The ITRS R consists of the following rules:
732_0_length_NULL(NULL) → 775_0_length_Return

The integer pair graph contains the following rules and edges:
(0): 816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
(1): 732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
(2): 732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

(0) -> (1), if ((x0[0] →^* java.lang.Object(List(x0[1]))))

(0) -> (2), if ((x0[0] →^* java.lang.Object(List(x0[2]))))

(1) -> (1), if ((x0[1] →^* java.lang.Object(List(x0[1]'))))

(1) -> (2), if ((x0[1] →^* java.lang.Object(List(x0[2]))))

(2) -> (0), if ((x0[2] →^* x0[0]))

The set Q consists of the following terms:
732_0_length_NULL(NULL)

(15) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

The TRS R consists of the following rules:

732_0_length_NULL(NULL) → 775_0_length_Return

The set Q consists of the following terms:

732_0_length_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(17) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

R is empty.
The set Q consists of the following terms:

732_0_length_NULL(NULL)

We have to consider all minimal (P,Q,R)-chains.

(19) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

732_0_length_NULL(NULL)

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

732_0_LENGTH_NULL(java.lang.Object(List(x0[2]))) → 816_0_LENGTH_STORE(x0[2])
The graph contains the following edges 1 > 1
732_0_LENGTH_NULL(java.lang.Object(List(x0[1]))) → 732_0_LENGTH_NULL(x0[1])
The graph contains the following edges 1 > 1
816_0_LENGTH_STORE(x0[0]) → 732_0_LENGTH_NULL(x0[0])
The graph contains the following edges 1 >= 1

(22) YES

(23) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(x0[0] > 0, x0[0])
(1): COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(x0[1] + -1)

(0) -> (1), if ((x0[0] > 0 →^* TRUE)∧(x0[0] →^* x0[1]))

(1) -> (0), if ((x0[1] + -1 →^* x0[0]))

The set Q is empty.

(24) IDPNonInfProof (SOUND transformation)

We consider the chain 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0]), COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1)) which results in the following constraint:
(1)    (>(x0[0], 0)=TRUE∧x0[0]=x0[1] ⇒ 398_0_MK_INC(x0[0])≥NonInfC∧398_0_MK_INC(x0[0])≥COND_398_0_MK_INC(>(x0[0], 0), x0[0])∧(U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (1) using rule (IV) which results in the following new constraint:
(2)    (>(x0[0], 0)=TRUE ⇒ 398_0_MK_INC(x0[0])≥NonInfC∧398_0_MK_INC(x0[0])≥COND_398_0_MK_INC(>(x0[0], 0), x0[0])∧(U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-1] ≥ 0 ⇒ (U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0 ⇒ (U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)

For Pair COND_398_0_MK_INC(TRUE, x0) → 398_0_MK_INC(+(x0, -1)) the following chains were created:

We consider the chain COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1)) which results in the following constraint:
(7)    (COND_398_0_MK_INC(TRUE, x0[1])≥NonInfC∧COND_398_0_MK_INC(TRUE, x0[1])≥398_0_MK_INC(+(x0[1], -1))∧(U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ((U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ((U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ((U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧[2 + (-1)bso_11] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    ((U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

398_0_MK_INC(x0) → COND_398_0_MK_INC(>(x0, 0), x0)
- (x0[0] ≥ 0 ⇒ (U^Increasing(COND_398_0_MK_INC(>(x0[0], 0), x0[0])), ≥)∧[(-1)Bound*bni_8 + (2)bni_8] + [(2)bni_8]x0[0] ≥ 0∧[(-1)bso_9] ≥ 0)
COND_398_0_MK_INC(TRUE, x0) → 398_0_MK_INC(+(x0, -1))
- ((U^Increasing(398_0_MK_INC(+(x0[1], -1))), ≥)∧0 = 0∧[2 + (-1)bso_11] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(398_0_MK_INC(x₁)) = [2]x₁
POL(COND_398_0_MK_INC(x₁, x₂)) = [2]x₂
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]

The following pairs are in P_>:

COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(+(x0[1], -1))

The following pairs are in P_bound:

398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0])

The following pairs are in P_≥:

398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(>(x0[0], 0), x0[0])

There are no usable rules.

(25) Complex Obligation (AND)

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 398_0_MK_INC(x0[0]) → COND_398_0_MK_INC(x0[0] > 0, x0[0])

The set Q is empty.

(27) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(28) TRUE

(29) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(1): COND_398_0_MK_INC(TRUE, x0[1]) → 398_0_MK_INC(x0[1] + -1)

The set Q is empty.

(30) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(31) TRUE

(32) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(1): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
(2): COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2] + 1, x1[2])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(0) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →^* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x5[0] →^* x4[1])∧(0 →^* x6[1])∧(x0[0] →^* x5[1]))

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →^* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0] →^* x4[3])∧(0 →^* x6[3])∧(x0[0] →^* x5[3]))

(1) -> (2), if ((x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1 →^* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))) →^* java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))))∧(x4[1] →^* x4[2])∧(x6[1] →^* x6[2])∧(x5[1] →^* x5[2]))

(2) -> (0), if ((893_0_length_ConstantStackPush(x1[2]) →^* 775_0_length_Return(x0[0]))∧(java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))) →^* java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))))∧(x4[2] + 1 →^* x5[0])∧(x1[2] →^* x2[0]))

(3) -> (4), if ((x6[3] < x5[3] →^* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))) →^* java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))))∧(x4[3] →^* x4[4])∧(x6[3] →^* x6[4])∧(x5[3] →^* x5[4]))

(4) -> (5), if ((1243_0_bubble_Load(x1[4]) →^* 3425_0_bubble_Return)∧(java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))) →^* java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))))∧(x4[4] →^* x4[5])∧(x5[4] →^* x5[5])∧(x6[4] →^* x6[5])∧(x1[4] →^* x1[5]))

(5) -> (6), if ((x6[5] >= 0 →^* TRUE)∧(java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))) →^* java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))))∧(x4[5] →^* x4[6])∧(x5[5] →^* x5[6])∧(x6[5] →^* x6[6])∧(x1[5] →^* x1[6]))

(6) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →^* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x4[6] →^* x4[1])∧(x6[6] + 1 →^* x6[1])∧(x5[6] →^* x5[1]))

(6) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))) →^* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x4[6] →^* x4[3])∧(x6[6] + 1 →^* x6[3])∧(x5[6] →^* x5[3]))

The set Q consists of the following terms:
893_0_length_ConstantStackPush(x0)
1243_0_bubble_Load(x0)
3413_0_bubble_NULL(NULL)
3413_0_bubble_NULL(java.lang.Object(List))
3723_0_bubble_LE(x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1)
3728_0_bubble_LE(x0, x1)
732_0_length_NULL(x0, NULL)
732_0_length_NULL(x0, java.lang.Object(List))
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1)
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List))
3513_0_bubble_Return

(33) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0), java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, x2) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, 0, x0) the following chains were created:

We consider the chain 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0]) which results in the following constraint:
(1)    (893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0])≥NonInfC∧893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])∧(U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧[(-1)bso_42] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE(&&(&&(>=(x6, x5), >=(x4, 0)), >(3, +(x4, 1))), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) the following chains were created:

We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]), COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2]) which results in the following constraint:
(6)    (&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1)))=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1])))=java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2])))∧x4[1]=x4[2]∧x6[1]=x6[2]∧x5[1]=x5[2] ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])∧(U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥))

We simplified constraint (6) using rules (I), (II), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(7)    (>(3, +(x4[1], 1))=TRUE∧>=(x6[1], x5[1])=TRUE∧>=(x4[1], 0)=TRUE ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])≥COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])∧(U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    ([1] + [-1]x4[1] ≥ 0∧x6[1] + [-1]x5[1] ≥ 0∧x4[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

We simplified constraint (10) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(11)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

We simplified constraint (11) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(12)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

(13)    ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)

For Pair COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), +(x4, 1), x1) the following chains were created:

We consider the chain COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2]) which results in the following constraint:
(14)    (COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2])≥NonInfC∧COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2])≥893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])∧(U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    ((U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    ((U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    ((U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧[1 + (-1)bso_46] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    ((U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_46] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE1(<(x6, x5), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) the following chains were created:

We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(19)    (<(x6[3], x5[3])=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]∧x6[3]=x6[4]∧x5[3]=x5[4] ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (19) using rules (I), (II), (IV) which results in the following new constraint:
(20)    (<(x6[3], x5[3])=TRUE ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(22)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(23)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47 + (-1)Bound*bni_47] + [(-1)bni_47]x4[3] ≥ 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(24)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (24) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(25)    (x5[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(26)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

(27)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)

For Pair COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) the following chains were created:

We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(28)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

We simplified constraint (28) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(29)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

We simplified constraint (29) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(30)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

We simplified constraint (30) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(31)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_50] ≥ 0)

We simplified constraint (31) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(32)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)

For Pair 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6, 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) the following chains were created:

We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(33)    (>=(x6[5], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]∧x5[5]=x5[6]∧x6[5]=x6[6]∧x1[5]=x1[6] ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (33) using rules (I), (II), (IV) which results in the following new constraint:
(34)    (>=(x6[5], 0)=TRUE ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (34) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(35)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (35) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(36)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (36) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(37)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_51 + (-1)Bound*bni_51] + [(-1)bni_51]x4[5] ≥ 0∧[(-1)bso_52] ≥ 0)

We simplified constraint (37) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(38)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧0 = 0∧[(-1)bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)

For Pair COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7, x2, x3))), x4, +(x6, 1), x5) the following chains were created:

We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(39)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

We simplified constraint (39) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(40)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (40) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(41)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (41) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(42)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[(-1)bso_54] ≥ 0)

We simplified constraint (42) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(43)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0), java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, x2) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2, x3, x4))), x5, 0, x0)
- ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_42] ≥ 0)
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE(&&(&&(>=(x6, x5), >=(x4, 0)), >(3, +(x4, 1))), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5)
- ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)
- ([1] + [-1]x4[1] ≥ 0∧x6[1] ≥ 0∧x4[1] ≥ 0∧x5[1] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])), ≥)∧[(-1)bni_43 + (-1)Bound*bni_43] + [(-1)bni_43]x4[1] ≥ 0∧[(-1)bso_44] ≥ 0)
COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), +(x4, 1), x1)
- ((U^Increasing(893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_46] ≥ 0)
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → COND_1190_0_MAIN_GE1(<(x6, x5), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5)
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_47] = 0∧[(-1)bni_47 + (-1)Bound*bni_47] ≥ 0∧0 = 0∧[(-1)bso_48] ≥ 0)
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x6, x5) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1), java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1)
- ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_50] ≥ 0)
1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6, 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1)
- (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧0 = 0∧[(-1)bni_51] = 0∧[(-1)bni_51 + (-1)Bound*bni_51] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_52] ≥ 0)
COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1, x2, x3))), x4, x5, x6, x1) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7, x2, x3))), x4, +(x6, 1), x5)
- ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_54] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(893_0_length_ConstantStackPush(x₁)) = [-1]
POL(732_0_length_NULL(x₁, x₂)) = [-1] + [-1]x₁
POL(0) = 0
POL(1243_0_bubble_Load(x₁)) = [-1]
POL(3413_0_bubble_NULL(x₁)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(3728_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_3723_0_bubble_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(>=(x₁, x₂)) = [-1]
POL(<(x₁, x₂)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(775_0_length_Return(x₁)) = x₁
POL(805_1_length_InvokeMethod(x₁, x₂)) = [-1] + [-1]x₂
POL(805_0_getTail_Return(x₁)) = [-1]
POL(Cond_805_1_length_InvokeMethod(x₁, x₂, x₃)) = [-1] + [-1]x₃
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(Cond_732_0_length_NULL(x₁, x₂, x₃)) = [-1] + [-1]x₂
POL(893_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃
POL(ARRAY(x₁)) = [-1]
POL(DATA_3(x₁, x₂, x₃)) = [-1]
POL(1190_0_MAIN_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂
POL(COND_1190_0_MAIN_GE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(3) = [3]
POL(COND_1190_0_MAIN_GE1(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₃
POL(1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆)) = [-1] + [-1]x₃
POL(COND_1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = [-1] + [-1]x₄

The following pairs are in P_>:

COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), +(x4[2], 1), x1[2])

The following pairs are in P_bound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])

The following pairs are in P_≥:

893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(&&(&&(>=(x6[1], x5[1]), >=(x4[1], 0)), >(3, +(x4[1], 1))), java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

There are no usable rules.

(34) Complex Obligation (AND)

(35) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer, Boolean

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(1): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1]) → COND_1190_0_MAIN_GE(x6[1] >= x5[1] && x4[1] >= 0 && 3 > x4[1] + 1, java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))), x4[1], x6[1], x5[1])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(0) -> (1), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →^* java.lang.Object(ARRAY(DATA_3(x1[1], x2[1], x3[1]))))∧(x5[0] →^* x4[1])∧(0 →^* x6[1])∧(x0[0] →^* x5[1]))

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →^* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0] →^* x4[3])∧(0 →^* x6[3])∧(x0[0] →^* x5[3]))

(36) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(37) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(38) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(39) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(40) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) the following chains were created:

We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(1)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_25] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)

For Pair 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) the following chains were created:

We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(6)    (>=(x6[5], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]∧x5[5]=x5[6]∧x6[5]=x6[6]∧x1[5]=x1[6] ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (6) using rules (I), (II), (IV) which results in the following new constraint:
(7)    (>=(x6[5], 0)=TRUE ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [bni_26]x5[5] + [(-1)bni_26]x6[5] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x6[5] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)

For Pair COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) the following chains were created:

We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(12)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_29] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) the following chains were created:

We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(17)    (<(x6[3], x5[3])=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]∧x6[3]=x6[4]∧x5[3]=x5[4] ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (17) using rules (I), (II), (IV) which results in the following new constraint:
(18)    (<(x6[3], x5[3])=TRUE ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_30 + (-1)Bound*bni_30] + [(-1)bni_30]x6[3] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(22)    (x5[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(23)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

(24)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])
- ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_25] ≥ 0)
1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
- (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x6[5] ≥ 0∧0 = 0∧[(-1)bso_27] ≥ 0)
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
- ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_29] ≥ 0)
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_30] + [bni_30]x5[3] ≥ 0∧[(-1)bso_31] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(1243_0_bubble_Load(x₁)) = [-1]
POL(3413_0_bubble_NULL(x₁)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_3723_0_bubble_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(>=(x₁, x₂)) = [-1]
POL(3728_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(<(x₁, x₂)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(COND_1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = [-1] + x₅ + [-1]x₆
POL(ARRAY(x₁)) = [-1]
POL(DATA_3(x₁, x₂, x₃)) = [-1]
POL(1190_0_MAIN_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₄
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆)) = [-1] + x₄ + [-1]x₅
POL(0) = 0
POL(COND_1190_0_MAIN_GE1(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₅ + [-1]x₄

The following pairs are in P_>:

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

The following pairs are in P_bound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

The following pairs are in P_≥:

1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

There are no usable rules.

(41) Complex Obligation (AND)

(42) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(43) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(44) TRUE

(45) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(46) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(47) TRUE

(48) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(0): 893_1_MAIN_INVOKEMETHOD(775_0_length_Return(x0[0]), java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], x2[0]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))), x5[0], 0, x0[0])
(2): COND_1190_0_MAIN_GE(TRUE, java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2], x6[2], x5[2]) → 893_1_MAIN_INVOKEMETHOD(893_0_length_ConstantStackPush(x1[2]), java.lang.Object(ARRAY(DATA_3(x1[2], x2[2], x3[2]))), x4[2] + 1, x1[2])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])

(0) -> (3), if ((java.lang.Object(ARRAY(DATA_3(x2[0], x3[0], x4[0]))) →^* java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))))∧(x5[0] →^* x4[3])∧(0 →^* x6[3])∧(x0[0] →^* x5[3]))

(49) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(50) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
893_0_length_ConstantStackPush(x0) → 732_0_length_NULL(0, x0)
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
732_0_length_NULL(x0, NULL) → 775_0_length_Return(x0)
732_0_length_NULL(x0, java.lang.Object(List)) → 805_1_length_InvokeMethod(805_0_getTail_Return(x1), x0)
805_1_length_InvokeMethod(805_0_getTail_Return(x0), x1) → Cond_805_1_length_InvokeMethod(x1 >= 0, 805_0_getTail_Return(x0), x1)
Cond_805_1_length_InvokeMethod(TRUE, 805_0_getTail_Return(x0), x1) → 732_0_length_NULL(x1 + 1, x0)
732_0_length_NULL(x0, java.lang.Object(List)) → Cond_732_0_length_NULL(x0 >= 0, x0, java.lang.Object(List))
Cond_732_0_length_NULL(TRUE, x0, java.lang.Object(List)) → 732_0_length_NULL(x0 + 1, x1)
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(6): COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], x6[6] + 1, x5[6])
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(51) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(52) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(53) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) the following chains were created:

We consider the chain COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(1)    (COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥NonInfC∧COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6])≥1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])∧(U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥))

We simplified constraint (1) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(2)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (2) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(3)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (3) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(4)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧[1 + (-1)bso_22] ≥ 0)

We simplified constraint (4) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(5)    ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)

We consider the chain 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]), COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6]) which results in the following constraint:
(6)    (>=(x6[5], 0)=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5])))=java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6])))∧x4[5]=x4[6]∧x5[5]=x5[6]∧x6[5]=x6[6]∧x1[5]=x1[6] ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (6) using rules (I), (II), (IV) which results in the following new constraint:
(7)    (>=(x6[5], 0)=TRUE ⇒ 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥NonInfC∧1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])≥COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])∧(U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥))

We simplified constraint (7) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(8)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (8) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(9)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (9) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(10)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[(-1)bni_23 + (-1)Bound*bni_23] + [bni_23]x5[5] + [(-1)bni_23]x6[5] ≥ 0∧[(-1)bso_24] ≥ 0)

We simplified constraint (10) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(11)    (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x6[5] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)

We consider the chain COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(12)    (COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥NonInfC∧COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4])≥1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])∧(U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥))

We simplified constraint (12) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(13)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

We simplified constraint (13) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(14)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

We simplified constraint (14) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(15)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧[(-1)bso_26] ≥ 0)

We simplified constraint (15) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(16)    ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)

We consider the chain 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]), COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4]) which results in the following constraint:
(17)    (<(x6[3], x5[3])=TRUE∧java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3])))=java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4])))∧x4[3]=x4[4]∧x6[3]=x6[4]∧x5[3]=x5[4] ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (17) using rules (I), (II), (IV) which results in the following new constraint:
(18)    (<(x6[3], x5[3])=TRUE ⇒ 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥NonInfC∧1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])≥COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])∧(U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥))

We simplified constraint (18) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(19)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (19) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(20)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (20) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(21)    (x5[3] + [-1] + [-1]x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)bni_27 + (-1)Bound*bni_27] + [(-1)bni_27]x6[3] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (21) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(22)    (x5[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

We simplified constraint (22) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(23)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

(24)    (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])
- ((U^Increasing(1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])), ≥)∧0 = 0∧0 = 0∧[1 + (-1)bso_22] ≥ 0)
1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
- (x6[5] ≥ 0 ⇒ (U^Increasing(COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])), ≥)∧[bni_23] = 0∧[(-1)bni_23 + (-1)Bound*bni_23] + [(-1)bni_23]x6[5] ≥ 0∧0 = 0∧[(-1)bso_24] ≥ 0)
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
- ((U^Increasing(1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])), ≥)∧0 = 0∧0 = 0∧[(-1)bso_26] ≥ 0)
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)
- (x5[3] ≥ 0∧x6[3] ≥ 0 ⇒ (U^Increasing(COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])), ≥)∧[(-1)Bound*bni_27] + [bni_27]x5[3] ≥ 0∧[(-1)bso_28] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(1243_0_bubble_Load(x₁)) = [-1]
POL(3413_0_bubble_NULL(x₁)) = [-1]
POL(NULL) = [-1]
POL(3425_0_bubble_Return) = [-1]
POL(java.lang.Object(x₁)) = [-1]
POL(List) = [-1]
POL(3723_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(Cond_3723_0_bubble_LE(x₁, x₂, x₃)) = [-1] + [-1]x₃ + [-1]x₂
POL(>=(x₁, x₂)) = [-1]
POL(3728_0_bubble_LE(x₁, x₂)) = [-1] + [-1]x₂ + [-1]x₁
POL(<(x₁, x₂)) = [-1]
POL(3513_0_bubble_Return) = [-1]
POL(COND_1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = [-1] + x₅ + [-1]x₆
POL(ARRAY(x₁)) = [1]
POL(DATA_3(x₁, x₂, x₃)) = [-1]
POL(1190_0_MAIN_GE(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₄
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(1243_1_MAIN_INVOKEMETHOD(x₁, x₂, x₃, x₄, x₅, x₆)) = [-1] + x₄ + [-1]x₅
POL(0) = 0
POL(COND_1190_0_MAIN_GE1(x₁, x₂, x₃, x₄, x₅)) = [-1] + x₅ + [-1]x₄

The following pairs are in P_>:

COND_1243_1_MAIN_INVOKEMETHOD(TRUE, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[6], x2[6], x3[6]))), x4[6], x5[6], x6[6], x1[6]) → 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x7[6], x2[6], x3[6]))), x4[6], +(x6[6], 1), x5[6])

The following pairs are in P_bound:

1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

The following pairs are in P_≥:

1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(>=(x6[5], 0), 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(<(x6[3], x5[3]), java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

There are no usable rules.

(54) Complex Obligation (AND)

(55) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
1243_0_bubble_Load(x0) → 3413_0_bubble_NULL(x0)
3413_0_bubble_NULL(NULL) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3425_0_bubble_Return
3413_0_bubble_NULL(java.lang.Object(List)) → 3723_0_bubble_LE(x0, x1)
3723_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 >= x0, x0, x1)
Cond_3723_0_bubble_LE(TRUE, x0, x1) → 3413_0_bubble_NULL(java.lang.Object(List))
3413_0_bubble_NULL(java.lang.Object(List)) → 3728_0_bubble_LE(x0, x1)
3728_0_bubble_LE(x0, x1) → Cond_3723_0_bubble_LE(x1 < x0, x0, x1)
3413_0_bubble_NULL(java.lang.Object(List)) → 3513_0_bubble_Return
3513_0_bubble_Return → 3425_0_bubble_Return

The integer pair graph contains the following rules and edges:
(5): 1243_1_MAIN_INVOKEMETHOD(3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5]) → COND_1243_1_MAIN_INVOKEMETHOD(x6[5] >= 0, 3425_0_bubble_Return, java.lang.Object(ARRAY(DATA_3(x1[5], x2[5], x3[5]))), x4[5], x5[5], x6[5], x1[5])
(4): COND_1190_0_MAIN_GE1(TRUE, java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x6[4], x5[4]) → 1243_1_MAIN_INVOKEMETHOD(1243_0_bubble_Load(x1[4]), java.lang.Object(ARRAY(DATA_3(x1[4], x2[4], x3[4]))), x4[4], x5[4], x6[4], x1[4])
(3): 1190_0_MAIN_GE(java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3]) → COND_1190_0_MAIN_GE1(x6[3] < x5[3], java.lang.Object(ARRAY(DATA_3(x1[3], x2[3], x3[3]))), x4[3], x6[3], x5[3])

(56) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(57) TRUE

(58) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

(59) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(0) Obligation:

(1) JBC2FIG (SOUND transformation)

(2) Obligation:

(3) FIGtoITRSProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) IDPNonInfProof (SOUND transformation)

(7) Complex Obligation (AND)

(8) Obligation:

(9) IDependencyGraphProof (EQUIVALENT transformation)

(10) TRUE

(11) Obligation:

(12) IDependencyGraphProof (EQUIVALENT transformation)

(13) TRUE

(14) Obligation:

(15) IDPtoQDPProof (SOUND transformation)

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) QReductionProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) IDPNonInfProof (SOUND transformation)

(25) Complex Obligation (AND)

(26) Obligation:

(27) IDependencyGraphProof (EQUIVALENT transformation)

(28) TRUE

(29) Obligation:

(30) IDependencyGraphProof (EQUIVALENT transformation)

(31) TRUE

(32) Obligation:

(33) IDPNonInfProof (SOUND transformation)

(34) Complex Obligation (AND)

(35) Obligation:

(36) IDependencyGraphProof (EQUIVALENT transformation)

(37) Obligation:

(38) UsableRulesProof (EQUIVALENT transformation)

(39) Obligation:

(40) IDPNonInfProof (SOUND transformation)

(41) Complex Obligation (AND)

(42) Obligation:

(43) IDependencyGraphProof (EQUIVALENT transformation)

(44) TRUE

(45) Obligation:

(46) IDependencyGraphProof (EQUIVALENT transformation)

(47) TRUE

(48) Obligation:

(49) IDependencyGraphProof (EQUIVALENT transformation)

(50) Obligation:

(51) UsableRulesProof (EQUIVALENT transformation)

(52) Obligation:

(53) IDPNonInfProof (SOUND transformation)

(54) Complex Obligation (AND)

(55) Obligation:

(56) IDependencyGraphProof (EQUIVALENT transformation)

(57) TRUE

(58) Obligation:

(59) IDependencyGraphProof (EQUIVALENT transformation)

(60) TRUE